Nuprl Lemma : ma-single-pre1_wf2
0,22
postcript
pdf
T
,
T'
:Type,
x
,
a
:Id,
P
:(
T
T'
Prop). ma-single-pre1(
x
;
T
;
a
;
T'
;
x
,
v
.
P
(
x
,
v
))
MsgA
latex
Definitions
ma-single-pre1(
x
;
A
;
a
;
T
;
y
,
v
.
P
(
y
;
v
))
,
x
:
A
.
B
(
x
)
,
x
,
y
.
t
(
x
;
y
)
,
x
(
s1
,
s2
)
,
Prop
,
Id
,
t
T
Lemmas
Id
wf
,
ma-single-pre1
wf
origin
T, T':Type, x, a:Id, P:(T
T'Prop). ma-single-pre1(x;T;a;T';x,v.P(x,v)) 
MsgA T, T':Type, x, a:Id, P:(TT'Prop). ma-single-pre1(x;T;a;T';x,v.P(x,v)) MsgA x:A. B(x)
x,y. t(x;y) T